\begin{tabbing}
ecl{-}machine2($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it upd}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$$z$$\in$update{-}spec{-}vars(${\it upd}$).R{-}state{-}var(\=$i$;fpf{-}join(IdDeq;${\it ds}$;$x$ : $T$);${\it da}$;$z$;fpf{-}ap(\=${\it ds}$;\+\+
\\[0ex]IdDeq;
\\[0ex]$z$);${\it ks}$;
\-\\[0ex]$\lambda$$k$,$s$,$v$,${\it z'}$.
\\[0ex]list\_accum(\=${\it z'}$,${\it nf}$.\=${\it nf}$/$n$,$f$.\+\+
\\[0ex]if $a$($n$,$k$,$s$,$v$,$s$($x$))$\rightarrow$ $f$($s$,$v$)
\\[0ex]else ${\it z'}$ fi;
\-\\[0ex]${\it z'}$;
\\[0ex]fpf{-}cap(${\it upd}$;product{-}deq(Knd;Id;KindDeq;IdDeq);\=$\langle$$k$\+
\\[0ex]$,\,$$z$$\rangle$;nil)))
\-\-\-
\end{tabbing}